(declare-fun s0 () String)
(declare-fun s1 () Int)
(assert (< s1 (str.len s0)))
(assert (<= 0 s1))
(assert (not (str.prefixof (str.substr s0 0 s1) s0)))
(check-sat)
(reset)

(set-option :produce-models true)
(set-logic ALL)
(declare-fun s0 () String)
(declare-fun s1 () Int)
(define-fun s2 () Int (str.len s0))
(define-fun s3 () Bool (<= s1 s2))
(define-fun s4 () Bool (not s3))
(define-fun s6 () Bool (<= s1 0))
(define-fun s8 () Bool (>= s1 s2))
(define-fun s9 () String (str.substr s0 0 s1))
(define-fun s10 () String (ite s8 s0 s9))
(define-fun s11 () String (ite s6 "" s10))
(define-fun s12 () Bool (str.prefixof s11 s0))
(define-fun s13 () Bool (or s4 s12))
(assert (not s13))
(check-sat)
(reset)


(declare-fun s0 () String)
(declare-fun s1 () Int)
(assert (< (str.len s0) 20))
(assert (not (str.prefixof (ite (<= s1 0) "" (ite (>= s1 (str.len s0)) s0 (str.substr s0 0 s1))) s0)))
(check-sat)
(reset)

(declare-fun s0 () String)
(declare-fun s1 () Int)
(assert (not (str.prefixof (ite (<= s1 0) "" (ite (>= s1 (str.len s0)) s0 (str.substr s0 0 s1))) s0)))
(check-sat)
(reset)
